module Flminimodelcheckerv2 where

import Data.List

-- Type Definition
type Node = Int
type Edge = (Node, Node)
type Graph = ([Node], [Edge])

-- Function Definition:depthfirst
-- Require: a graph and a node representing the entry point
-- Return: a list nodes reachable from the entry point node
depthfirst :: Graph -> Node -> [Node]
depthfirst (v, e) n
	| [x | x <- v, x == n] == [] = []
	| otherwise = dfrecursive (v, e) [n]

-- Function Definition:	dfrecursive
-- Require: a graph and a stack initialized with only the entry point
-- Return:  a list of nodes arranged in visiting order
dfrecursive ::Graph -> [Node] -> [Node]
dfrecursive ([], _) _ = []
dfrecursive (_, _) [] = []
dfrecursive (v, e) (top : stack)
	| [x | x <- v, x == top] == [] = dfrecursive (newv, e) stack    -- 
	-- visit the top node
	| otherwise = top : dfrecursive (newv, e) (adjacent ++ stack)   
	where 
		adjacent = [x | (x, y) <- e, y == top] ++ [x | (y, x) <- e , y == top]
		-- delete the recently visited node
		newv = [x | x <- v, x /= top]